\begin{tabbing}
state{-}machine{-}spec\=\{i:l\}\+
\\[0ex](${\it es}$; $C$; $R$; $F$; $I$; $O$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=$X$:AbsInterface(${\it es}$;$C$)\+
\\[0ex]$\exists$\=$Q$:es{-}E(${\it es}$)$\rightarrow$es{-}E(${\it es}$)$\rightarrow\mathbb{P}$\{i\}\+
\\[0ex]$\exists$\=$B$:retrace(${\it es}$; $Q$; $X$)\+
\\[0ex](Q{-}R{-}glued(${\it es}$; $C$; ($\lambda$$e$.$I$($e$)); $I$; ($\lambda$$e$,${\it e'}$. es{-}locl(${\it es}$; $e$; ${\it e'}$)); $X$; $Q$)
\\[0ex]\& Q{-}R{-}glued(\=${\it es}$;\+
\\[0ex]$R$;
\\[0ex]($\lambda$$e$.$F$(map($\lambda$${\it e'}$.$X$(${\it e'}$);(retracer($B$)($e$)) @ [$e$ / []])));
\\[0ex]$X$;
\\[0ex]$Q$;
\\[0ex]$O$;
\\[0ex]($\lambda$$e$,${\it e'}$. (es{-}loc(${\it es}$; $e$) = es{-}loc(${\it es}$; ${\it e'}$) $\in$ Id) $\Rightarrow$ es{-}locl(${\it es}$; $e$; ${\it e'}$))))
\-\-\-\-
\end{tabbing}